\DeclareMathVersion{zed}
\SetMathAlphabet{\mathrm}{zed}{\encodingdefault}{\rmdefault}{m}{n}%
\SetMathAlphabet{\mathbf}{zed}{\encodingdefault}{\rmdefault}{bx}{n}%
\SetMathAlphabet{\mathsf}{zed}{\encodingdefault}{\sfdefault}{m}{n}%
\SetMathAlphabet{\mathtt}{zed}{\encodingdefault}{\ttdefault}{m}{n}%
\DeclareSymbolFont{italics}{\encodingdefault}{\rmdefault}{m}{it}%
\DeclareSymbolFontAlphabet{\mathrm}{operators}
\DeclareSymbolFontAlphabet{\mathit}{letters}
\DeclareSymbolFontAlphabet{\mathcal}{symbols}
\DeclareSymbolFont{lasy}{U}{lasy}{m}{n}
\DeclareSymbolFont{AMSa}{U}{msa}{m}{n}
\DeclareSymbolFont{AMSb}{U}{msb}{m}{n}
\let\mho\undefined
\let\Join\undefined
\let\Box\undefined
\let\Diamond\undefined
\let\leadsto\undefined
\let\sqsubset\undefined
\let\sqsupset\undefined
\let\lhd\undefined
\let\unlhd\undefined
\let\rhd\undefined
\let\unrhd\undefined
\DeclareMathSymbol{\mho}{\mathord}{lasy}{"30}
\DeclareMathSymbol{\Join}{\mathrel}{lasy}{"31}
\DeclareMathSymbol{\Box}{\mathord}{lasy}{"32}
\DeclareMathSymbol{\Diamond}{\mathord}{lasy}{"33}
\DeclareMathSymbol{\leadsto}{\mathrel}{lasy}{"3B}
\DeclareMathSymbol{\sqsubset}{\mathrel}{lasy}{"3C}
\DeclareMathSymbol{\sqsupset}{\mathrel}{lasy}{"3D}
\DeclareMathSymbol{\lhd}{\mathrel}{lasy}{"01}
\DeclareMathSymbol{\unlhd}{\mathrel}{lasy}{"02}
\DeclareMathSymbol{\rhd}{\mathrel}{lasy}{"03}
\DeclareMathSymbol{\unrhd}{\mathrel}{lasy}{"04}
\DeclareSymbolFontAlphabet{\bbold}{AMSb}
\mathversion{zed}


\def\@setmcodes#1#2#3{{\count0=#1 \count1=#3
    \loop \global\mathcode\count0=\count1 \ifnum \count0<#2
    \advance\count0 by1 \advance\count1 by1 \repeat}}
\@setmcodes{`A}{`Z}{"7\hexnumber@\symitalics41}% 
\@setmcodes{`a}{`z}{"7\hexnumber@\symitalics61}% 

\DeclareRobustCommand\em
        {\@nomath\em \ifdim \fontdimen\@ne\font >\z@
                       \upshape \else \slshape \fi}

% Now to give sensible names for Squiggol and category theory symbols

\def\implies{\Rightarrow}
\def\iff{\Leftrightarrow}
\def\concat{\mathbin{\plus\!\!\!\plus}}
\def\suchthat{\mathrel{|}}
\def\compose{\mathbin{\cdot}}
\def\set#1{\mathord{\{#1\}}}
\def\seq#1{\mathord{[#1]}}
\def\emptyseq{\seq{\,}}
\def\emptyrel{\emptyset}
\def\nilset{\set{\,}}

\newcommand{\split}[2]{\langle #1,#2\rangle}
\newcommand{\converse}[1]{#1^{\circ}}
\newcommand{\lbana}{\mbox{$(\![$}}
\newcommand{\rbana}{\mbox{$]\!)$}}
\newcommand{\lbcat}{\mbox{$[\!($}}
\newcommand{\rbcat}{\mbox{$)\!]$}}
\newcommand{\lccat}{\mbox{$[\!\langle$}}
\newcommand{\rccat}{\mbox{$\rangle\!]$}}
\newcommand{\cata}[1]{\mbox{$\lbana #1 \rbana$}}
\newcommand{\ana}[1]{\mbox{$\lbcat #1 \rbcat$}}
\newcommand{\cockett}[1]{\mbox{$\lccat #1 \rccat$}}
\newcommand{\spe}{\mbox{$\ni$}}
\newcommand{\eps}{\mbox{$\in$}}
\newcommand{\snoc}{\mathbin{+\!\!\!+\!\!\!<}}
\newcommand{\bnoc}{\mathbin{+\!\!\!<}}
\newcommand{\func}[1]{{\sf #1}}
\newcommand{\Pow}{{\sf P}}
\newcommand{\Ext}{{\sf E}}
\newcommand{\toprel}{\Pi}
\newcommand{\botrel}{0}
\newcommand{\id}{id}
\newcommand{\union}{\;\cup\;}
\newcommand{\bigunion}{\mbox{$\bigcup$}}
\newcommand{\bigmeet}{\mbox{$\bigcap$}}
\newcommand{\from}{\mathbin{\leftarrow}}
\newcommand{\terminator}{{1}}
\newcommand{\ffrom}{\Leftarrow}
\newcommand{\wfrom}{\hookleftarrow}
\newcommand{\wto}{\hookrightarrow}
\newcommand{\acc}[1]{\mbox{$\lfloor #1 \rfloor$}}
\newcommand{\bang}{\mbox{$!$}}
\newcommand{\bong}{\mbox{!`}}
\newcommand{\graph}{\mbox{\sf J}}
\newcommand{\sse}{\subseteq}
\newcommand{\spse}{\supseteq}
\newcommand{\wok}[1]{\mbox{${#1}^{\circ}$}}
\newcommand{\rtc}[1]{\mbox{${#1}^{\star}$}}
\newcommand{\conj}{\;\wedge\;}
\newcommand{\bs}{\mbox{$\backslash$}}
\newcommand{\dom}[1]{\mbox{${#1}\Box$}}
\newcommand{\ran}[1]{\mbox{$\Box{#1}$}}
\newcommand{\tgt}{\triangleleft}
\newcommand{\src}{\triangleright}
\newcommand{\floor}[1]{\lfloor #1 \rfloor}
\newcommand{\bscor}{\mathbin{\backslash\!\!\!\!-}}

% general utilities 

\def\emark{$\Box$}
\def\pause{\vspace{2ex}}
\def\text#1{\mbox{\rm #1}} 
\newcommand{\idisp}[1]{\makebox[0 in][l]{$#1$}}

% Make ~ do a thin space in maths mode. We need to insert a space between a
% function and its argument, because spaces aren't significant in maths mode.
% Thus, you say "f~x".

\let\twiddle=~
\def\applicationspace{\makebox[.15ex]{}}
\def~{\ifmmode \applicationspace \else \twiddle \fi}


% Make . active in maths mode, as a "compose". Save old . as \period
% Thus, you can say "map~tails . inits", and "3\period 14"

\mathchardef\period=\mathcode`. % ordinary symbol
{\catcode`.=\active \gdef.{\compose}}
\mathcode`.="8000

% Now define the abbreviations we will use. We have
%           =>     is an abbreviation for     \implies
%           <=              "                 \le
%           >=              "                 \ge
%           ++              "                 \concat
%           <=>             "                 \iff
%           ->              "                 \rightarrow

\mathchardef\equals=\mathcode`=
\mathcode`=="8000

{\catcode`==\active \gdef={\futurelet\@next\@newequals}}
\def\@newequals{\ifx>\@next \def\@next##1{\implies} 
                      \else \def\@next{\equals} 
                \fi 
                \@next}

\def\Relbar{\mathrel{=}} % \Relbar (in plain TeX) screwed up by making = active



\mathchardef\lessthan=\mathcode`<
\mathcode`<="8000

{\catcode`<=\active \gdef<{\futurelet\@next\@newlessthan}}
\def\@newlessthan{\ifx=\@next \def\@next##1{\futurelet\@next\@newle} 
                  \else \ifx<\@next \def\@next##1{\ll}
                              \else \def\@next{\lessthan} 
                        \fi
                  \fi 
                  \@next}

\def\@newle{\ifx>\@next \def\@next##1{\iff}
                  \else \def\@next{\le}
            \fi
            \@next}




\mathchardef\greaterthan=\mathcode`>
\mathcode`>="8000

{\catcode`>=\active \gdef>{\futurelet\@next\@newgreaterthan}}
\def\@newgreaterthan{\ifx=\@next \def\@next##1{\ge} 
                     \else \ifx>\@next \def\@next##1{\gg}
                                 \else \def\@next{\greaterthan} 
                           \fi
                     \fi 
                     \@next}


\mathchardef\plus=\mathcode`+
\mathcode`+="8000

{\catcode`+=\active \gdef+{\futurelet\@next\@newplus}}
\def\@newplus{\ifx+\@next \def\@next##1{\concat} 
                    \else \def\@next{\plus} 
              \fi 
              \@next}



\mathchardef\minus=\mathcode`-
\mathcode`-="8000

{\catcode`-=\active \gdef-{\futurelet\@next\@newminus}}
\def\@newminus{\ifx>\@next \def\@next##1{\rightarrow} 
                     \else \def\@next{\minus} 
                \fi 
                \@next}

% The derivation environment

\newenvironment{derivation}{\begin{eqnarray*}
                          }{\end{eqnarray*}
                            \global\@ignoretrue}
\def\given#1{&&\begin{array}[t]{@{}l@{}}%
                #1
               \end{array} \\ \nopagebreak}
\def\step{\@ifnextchar({\@step}{\@step(=)}}
\def\@step(#1)[#2]#3{&#1& \begin{oldtabular}[t]{@{}l@{}}%
                          \quad  \{#2\}
                          \end{oldtabular} \\
                     &  & \begin{array}[t]{@{}l@{}}%
                           #3  
                          \end{array} \\ }
\def\step{\@ifnextchar({\@step}{\@step(=)}}
\def\result{\@ifnextchar({\@result}{\@result(=)}}
\def\@result(#1)[#2]#3{&#1& \begin{oldtabular}[t]{@{}l@{}}%
                            \quad\{#2\}
                           \end{oldtabular} \\
                       &  & \begin{array}[t]{@{}l@{}}%
                             #3  
                            \end{array}  }

% Set up Theorems, Lemmas and Corollaries and Propositions:


\newtheorem{theorem}{Theorem}
\newtheorem{fact}{Fact}
\newtheorem{lemma}[fact]{Lemma}
\newtheorem{corollary}{Corollary}
\newtheorem{proposition}{Proposition}

%\newcounter{facts}
%\newenvironment{fact}{\begin{quote}\normalsize\sl
%                      \noindent{\bf Fact \refstepcounter{facts}\thefacts}}
%					 {\end{quote}}
%\newenvironment{lemma}{\begin{quote}\normalsize \sl
%                     \noindent{\bf Lemma \refstepcounter{facts}\thefacts}}
%					 {\end{quote}}
\newenvironment{refact}[1]{\begin{quote}\normalsize 
                     \noindent{\it Restatement of Fact #1.}}{\end{quote}}


\newenvironment{program}{\[\begin{array}{rcll}
                        }{\end{array}\]}


% common hyphenation exceptions:

\hyphenation{de-ter-mi-nism de-ter-mi-nistic non-de-ter-mi-nism}
\hyphenation{analy-sis}
\hyphenation{defi-ni-tion}
\hyphenation{lit-era-ture}
\hyphenation{cat-egory cat-egories cat-egorical}
\hyphenation{tabu-lation}
\hyphenation{equiv-al-ent equiv-al-ence}
\hyphenation{necess-ary}
\hyphenation{monic monics}
\hyphenation{op-er-ation}
\hyphenation{typi-cal}
\hyphenation{sum-mar-izing sum-mary}


\newdimen\mathindent
\AtEndOfClass{\mathindent\leftmargini}
\renewcommand{\[}{\relax
                 \ifmmode\@badmath
                 \else
                   \begin{trivlist}%
                     \@beginparpenalty\predisplaypenalty
                     \@endparpenalty\postdisplaypenalty
                     \item[]\leavevmode
                     \hbox to\linewidth\bgroup $\m@th\displaystyle %$
                       \hskip\mathindent\bgroup
                 \fi}
\renewcommand{\]}{\relax
                 \ifmmode
                       \egroup $\hfil% $
                     \egroup
                   \end{trivlist}%
                 \else \@badmath
                 \fi}
\renewenvironment{equation}%
    {\@beginparpenalty\predisplaypenalty
     \@endparpenalty\postdisplaypenalty
     \refstepcounter{equation}%
     \trivlist \item[]\leavevmode
       \hbox to\linewidth\bgroup $\m@th% $
         \displaystyle
         \hskip\mathindent}%
        {$\hfil % $
         \displaywidth\linewidth\hbox{\@eqnnum}%
       \egroup
     \endtrivlist}
\renewenvironment{eqnarray}{%
    \stepcounter{equation}%
    \def\@currentlabel{\p@equation\theequation}%
    \global\@eqnswtrue\m@th
    \global\@eqcnt\z@
    \tabskip\mathindent
    \let\\=\@eqncr
    \setlength{\abovedisplayskip}{\topsep}%
    \ifvmode
      \addtolength{\abovedisplayskip}{\partopsep}%
    \fi
    %    \addtolength{\abovedisplayskip}{\parskip}%
    \setlength{\belowdisplayskip}{\abovedisplayskip}%
    \setlength{\belowdisplayshortskip}{\abovedisplayskip}%
    \setlength{\abovedisplayshortskip}{\abovedisplayskip}%
    $$\everycr{}\halign to\linewidth% $$
    \bgroup
      \hskip\@centering
      $\displaystyle\tabskip\z@skip{##}$\@eqnsel&%
      \global\@eqcnt\@ne \hskip \tw@\arraycolsep \hfil${##}$\hfil&%
      \global\@eqcnt\tw@ \hskip \tw@\arraycolsep
        $\displaystyle{##}$\hfil \tabskip\@centering&%
      \global\@eqcnt\thr@@
        \hbox to \z@\bgroup\hss##\egroup\tabskip\z@skip\cr}%
      {\@@eqncr
    \egroup
    \global\advance\c@equation\m@ne$$% $$
    \global\@ignoretrue
    }
